i, a:Id, p:FinProbSpace, ds:x:Id fp Type, P:(State(ds)),
init:{f:x:Id fp ds(x)?Top| x:Id. (x  dom(ds))  (x  dom(f))} , es:ES.
pre-init-p2(es;i;ds;init;a;p;P)   

latex

Definitions	ff, tt, if b then t else f fi , x. t(x), A c B, P & Q, pre-init-p2(es;i;ds;init;a;p;P), , t  T, P  Q, f(x)?z, x:A. B(x), False, A, P  Q, Unit, x(s), ,
Lemmas	finite-prob-space wf, decl-state wf, Id wf, fpf wf, event system wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, subtype rel self, eqtt to assert, bool wf, fpf-trivial-subtype-top, fpf-dom wf, top wf, id-deq wf, fpf-cap wf, fpf-ap wf, init-p wf, pre-init-p wf